2025-10-01 Inversion & Structural Rules
Inversion
Syntax directed means for each type, there’s only rule that can introduce it. E.g. the only way to introduce the plus syntax is using the PLUS rule.
We call these inversion lemmata:
%%🖋 Edit in Excalidraw%%
Can be proven by (but doesn’t need to proven in exam):
- Proof by Induction
- Inspection
Weakening
Adding unrelated variables to the environment should not affect typing. Holds for most programming languages.
If you end up with two different environments, you can use weakening.
%%Substitution
Substitution is a [[meta-theoretic operation]]. 
%%🖋 Edit in Excalidraw%%
Barendregt Convention
We assume that everything has been alpha renamed already so this doesn’t happen. Basically we just assume this won’t be a problem.
Substitution Lemma
To ensure substitution plays nicely with our language: 
%%🖋 Edit in Excalidraw%%